nLab function realizability

Related concepts

• realizability

• Kleene's second algebra

The subcategory on the effectively computable morphisms of the function realizability topos $RT(\mathcal{K}_2)$ is the Kleene-Vesley topos $KV$. The category of “admissible representations” $AdmRep$ (whose morphisms are computable functions (analysis), see there) is a reflective subcategory of $RT(\mathcal{K}_2)$ (BSS 07) and the restriction of that to $KV$ is $AdmRep_{eff}$

$$\array{ AdmRep_{eff} &\hookrightarrow& KV \\ \downarrow && \downarrow \\ AdmRep &\hookrightarrow& RT(\mathcal{K}_2) }$$

computability

	type I computability	type II computability
typical domain	natural numbers $\mathbb{N}$	Baire space of infinite sequences $\mathbb{B} = \mathbb{N}^{\mathbb{N}}$
computable functions	partial recursive function	computable function (analysis)
type of computable mathematics	recursive mathematics	computable analysis, Type Two Theory of Effectivity
type of realizability	number realizability	function realizability
partial combinatory algebra	Kleene's first partial combinatory algebra	Kleene's second partial combinatory algebra

References

• Thomas Streicher, around p. 17 of Realizability (2017/18) (pdf)

• Jaap van Oosten, Realizability: an introduction to its categorical side, Studies in Logic and the Foundations of Mathematics, vol. 152, Elsevier, 2008 (preface pdf)

• Ingo Battenfeld, Matthias Schröder, Alex Simpson, A convenient category of domains, in L. Cardelli, M. Fiore and G. Winskel (eds.), Computation, Meaning and Logic, Articles dedicated to Gordon Plotkin Electronic Notes in Computer Science, 34 pp., to appear, 2007 (pdf)

• Andrej Bauer and Andrew Swan, Every metric space is separable in function realizability, 2018, (arxiv:1804.00427)